Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	app(app(app(rec,f),x),0)	→ x
2:	app(app(app(rec,f),x),app(s,y))	→ app(app(f,app(s,y)),app(app(app(rec,f),x),y))

There are 3 dependency pairs:


3:	APP(app(app(rec,f),x),app(s,y))	→ APP(app(f,app(s,y)),app(app(app(rec,f),x),y))
4:	APP(app(app(rec,f),x),app(s,y))	→ APP(f,app(s,y))
5:	APP(app(app(rec,f),x),app(s,y))	→ APP(app(app(rec,f),x),y)

Consider the SCC {3-5}. The constraints could not be solved.

Tyrolean Termination Tool (0.04 seconds) --- May 4, 2006